Software contracts allow programmers to state rich program properties usingthe full expressive power of an object language. However, since they areenforced at runtime, monitoring contracts imposes significant overhead anddelays error discovery. So contract verification aims to guarantee all or mostof these properties ahead of time, enabling valuable optimizations and yieldinga more general assurance of correctness. Existing methods for static contractverification satisfy the needs of more restricted target languages, but fail toaddress the challenges unique to those conjoining untyped, dynamic programming,higher-order functions, modularity, and statefulness. Our approach tackles allthese features at once, in the context of the full Racket system---a matureenvironment for stateful, higher-order, multi-paradigm programming with orwithout types. Evaluating our method using a set of both pure and statefulbenchmarks, we are able to verify 99.94% of checks statically (all but 28 of49, 861). Stateful, higher-order functions pose significant challenges for staticcontract verification in particular. In the presence of these features, amodular analysis must permit code from the current module to escape permanentlyto an opaque context (unspecified code from outside the current module) thatmay be stateful and therefore store a reference to the escaped closure. Also,contracts themselves, being predicates wri en in unrestricted Racket, mayexhibit stateful behavior; a sound approach must be robust to contracts whichare arbitrarily expressive and interwoven with the code they monitor. In thispaper, we present and evaluate our solution based on higher-order symbolicexecution, explain the techniques we used to address such thorny issues,formalize a notion of behavioral approximation, and use it to provide amechanized proof of soundness.
展开▼
